Nuprl Lemma : locl_one_one 11,40

ab:Id. (locl(a) = locl(b Knd)  (a = b
latex


DefinitionsId, t  T, IdLnk, , P  Q, x:AB(x), locl(a), Knd
LemmasIdLnk wf, Id wf

origin